$\forall$${\it es}$:ES, $T$:Type, $X$:MaInterface($T$).
\\[0ex]ma{-}interface{-}consistent2(${\it es}$;$X$) $\Rightarrow$ ma{-}interface{-}consistent(${\it es}$;$X$)